Nuprl Definition : discrete_struct
11,40
postcript
pdf
DS(
A
) ==
sort
:(
A
Type)
(
a
:
A
EqDecider(
sort
(
a
)))
latex
clarification:
discrete_struct{i:l}(
A
) ==
sort
:(
A
Type{i})
(
a
:
A
EqDecider(
sort
(
a
)))
latex
Definitions
EqDecider(
T
)
FDL editor aliases
DS
origin
Type) 
(a:AEqDecider(sort(a)))
Type{i}) (a:AEqDecider(sort(a))) Type) (a:AEqDecider(sort(a)))
Type{i}) (a:AEqDecider(sort(a)))